| Definitions | s = t, t  T, ES, AbsInterface(A), sys-antecedent(es;Sys), E(X),  , x:A  B(x), a < b, P   Q,  x:A. B(x), {T}, x:A  B(x),  b, left + right, {x:A| B(x)} ,  x:A. B(x),  A, y is f*(x), Top, E, f(a), (e < e'), loc(e), Id,  , P & Q, let x,y = A in B(x;y), t.1, a:A fp B(a), strong-subtype(A;B), n+m, False, Type,  ,  , Outcome, #$n, A  B, !Void(),  , S  T, n - m, |g|, e < e', (x l), SWellFounded(R(x;y)), e  X, e c e', EState(T), EqDecider(T), Unit, IdLnk, EOrderAxioms(E; pred?; info), kindcase(k; a.f(a); l,t.g(l;t) ), Knd, loc(e), kind(e), Msg(M), type List, val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), r s, constant_function(f;A;B), pred!(e;e'),   x,y. t(x;y),  x:A.B(x), suptype(S; T), first(e), <a, b>, pred(e), x.A(x), x. t(x), i  j , -n, hd(l), y=f*(x) via L, Atom$n, A c B, f**(e), first(e), (e <loc e'), case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , source(l), destination(l), es-init(es;e), e loc e' , isrcv(e), kind(e), es-first-from(es;e;l;tg), isrcv(k), P  Q, P Q, lastchange(x;e), (last change to x before e), SQType(T), s ~ t, P  Q, Dec(P), Atom, {i..j }, x,y:A//B(x;y), b | a, a ~ b, |p|, a b, a <p b, a < b, x f y, |r|, xL. P(x), (xL.P(x)),  , r < s, q-rel(r;x), dstype(TypeNames; d; a), l_disjoint(T;l1;l2), MaName, e<e'.P(e), ee'.P(e), e<e'. P(e), ee'.P(e), e[e1,e2).P(e), e[e1,e2).P(e), e[e1,e2].P(e), e[e1,e2].P(e), e(e1,e2].P(e), a = b, True,  T, X(e), sender(e), SqStable(P), a =!x:T. Q(x), InvFuns(A;B;f;g), Inj(A;B;f), IsEqFun(T;eq), Refl(T;x,y.E(x;y)), Sym(T;x,y.E(x;y)), Trans(T;x,y.E(x;y)), AntiSym(T;x,y.R(x;y)), Connex(T;x,y.R(x;y)), CoPrime(a,b), Ident(T;op;id), Assoc(T;op), Comm(T;op), Inverse(T;op;id;inv), BiLinear(T;pl;tm), IsBilinear(A;B;C;+a;+b;+c;f), IsAction(A;x;e;S;f), Dist1op2opLR(A;1op;2op), fun_thru_1op(A;B;opa;opb;f), FunThru2op(A;B;opa;opb;f), Cancel(T;S;op), monot(T;x,y.R(x;y);f), IsMonoid(T;op;id), IsGroup(T;op;id;inv), IsMonHom{M1,M2}(f), a b, IsIntegDom(r), IsPrimeIdeal(R;P), f g, ff, inr x , tt, inl x |
| Lemmas | fun-connected transitivity, decidable assert, btrue wf, bfalse wf, sq stable from decidable, decidable es-causle, fun-connected-fixedpoint, squash wf, true wf, es-first wf, fun-connected-step-back, not functionality wrt iff, assert-eq-id, eq id wf, decidable equal Id, fun-connected-step, decidable wf, Id sq, iff wf, rev implies wf, es-isrcv-loc, es-le-loc, es-le wf, es-loc-pred, fun-connected weakening eq, fun-path wf, es-loc wf, es-E-interface-subtype rel, ge wf, nat properties, deq wf, EOrderAxioms wf, kind wf, Msg wf, val-axiom wf, cless wf, qle wf, bool wf, Knd wf, kindcase wf, IdLnk wf, constant function wf, loc wf, first wf, unit wf, pred! wf, strongwellfounded wf, rationals wf, EState wf, event system wf, es-interface wf, es-causle wf, sys-antecedent wf, assert wf, es-is-interface wf, top wf, es-causl-swellfnd, nat ind tp, Id wf, not wf, fun-connected wf, guard wf, es-causl wf, le wf, false wf, nat wf, member wf, es-E wf, es-E-interface wf, subtype rel wf |
